 $LOAD_PATH.unshift File.join(File.dirname(__FILE__),'../..','ext_pr1/lib')
 require 'ext_pr1_v4'
#Volume of a hollow cube
#hollow_cube_volume ::= (length_outer, length_inner)::
#                        Nat x Nat -> Nat where (length_outer >= length_inner)
#Test {(3,2)=>19,    (2,2) => 0, (0,0) => 0,
#('10', '5')=> Err, (5, '10')=>Err, (-1, 5) => Err, (3, -5)=>Err,
#(2,3)=>Err}

def hollow_cube_volume(length_outer, length_inner)
  check_pre((
      length_outer.nat? and length_inner.nat? and (length_outer >= length_inner)))
  cube_volume(length_outer) - cube_volume(length_inner)

end

def cube_volume(length)
  length ** 3
end